This section is intended to provide a background or context to the disclosed embodiments. The description herein may include concepts that could be pursued, but are not necessarily ones that have been previously conceived or pursued. Therefore, unless otherwise indicated herein, what is described in this section is not prior art to the description and claims in this application and is not admitted to be prior art by inclusion in this section.
Boolean Satisfiability (SAT) solvers are useful in a variety of problems. SAT problems arise in a number of arenas, the field of planning being an example of an important arena. As the demand for more efficient use of heterogeneous and interdependent resources has increased, so has the complexity of the constraint problems that must be solved to assign and employ those resources. With the increase in the complexity of the constraint problems that must be solved there have been significant increases in the challenges within the problem of finding feasible plans that make a highly efficient use of the available resources.
In the planning process a number of computerized techniques have been employed. For example, a common technique is to reduce the planning problem to the combination of a set of constraints and a fitness metric. The constraints capture plans that are consistent with the rules of the world in which the plan is to takes place. The fitness metric provides a means of ordering feasible plans based on desirability. In general, SAT solvers have long provided a means to find solutions to the constraint component. SAT solvers can also be used to find plans that satisfy constraints while meeting a certain fixed threshold of fitness.
However, a SAT solver typically lacks the ability to find an optimal solution, i.e., one that maximizes or minimizes a specified fitness metric while satisfying the constraints system, in a single step. Generally, a SAT solver is configured to find a solution at one fitness level, and is then repeatedly executed anew by requiring a higher fitness threshold in each iteration until a fitness level is reached for which the constraint system is satisfiable at that level, but unsatisfiable at any higher level. The solution that satisfies the constraints at the highest fitness level is determined to be the optimal solution.
SAT solvers typically require the constraint formulae to be expressed in the conjunctive normal form (CNF), which is a conjunction of clauses, where a clause is a disjunction of literals. A literal is either a variable name or its negation. A satisfying assignment of variables returned by the SAT solver corresponds to a plan of fitness greater than or equal to k. If the problem is unsatisfiable at fitness k, the SAT solver returns a proof that there are no plans of fitness greater than or equal to k.
Iterative Repair (IR) is a general mechanism that extends the normal capability of a SAT-solver so that it may address several additional application problem domains. For example, the IR capability is beneficial for applying a SAT solver in a domain where the environment may change. Changes in the environment are reflected as changes in the constraint system embodied in a logic formula being solved. The changes are typically provided by a driver application.
In many defense and commercial applications, the solution to a planning problem automatically rendered by a SAT solver is subject to manual review before a commitment to apply or execute the solution is made. The IR capability provides a mechanism for replanning, in part or in whole, if a change introduced by a manual review. However, SAT is an NP-complete problem (i.e., a class of problem for which only the solutions requiring exponential time are currently known). Solved iteratively for increasing fitness values, k, the IR can produce provably optimal solutions for NP-hard k-optimization problems (i.e., problems that are as hard as NP-complete problems). In this method, a SAT instance is modified for each k and is resolved producing a better solution until k reaches a level at which the problem is unsatisfiable, thus providing a proof of optimality. As described above, changing a fitness level can be analogized to modifying the problem in terms of its constraints. Managing the fitness levels to be tested and translating those levels into a modified problem is generally performed by a driver application. In these examples, the driver application interacts with the IR-enabled SAT solver.
The Davis-Putnam-Logemann-Loveland (DPLL) algorithm is a complete backtracking-based algorithm for deciding the satisfiability of propositional logic formulae in conjunctive normal form, i.e., for solving the CNF-SAT problem. The basic backtracking algorithm runs by choosing a branching literal, assigning a truth value to it, simplifying the formula, and then recursively checking if the simplified formula is satisfiable. If this is the case, the original formula is satisfiable; otherwise, the same recursive check is done assuming the opposite truth value. This is known as the splitting rule, as it splits the problem into two simpler sub-problems. The simplification step normally removes all clauses from the formula that become true under the assignment being tested, and all literals that become false from the remaining clauses.
Various improvements of the DPLL are known in the field. One such improvement is defining variants of the basic backtracking algorithm. Techniques in this area include non-chronological backtracking and clause learning. These refinements describe a method of backtracking after reaching a conflict which “learns” the root causes of the conflict (i.e., conflicting assignments to variables) in order to avoid reaching the same conflict again. Intuitively, backtracking can be viewed as jumping back to the root problem in a sequence of decisions and making the opposite decision.
In finding an optimal plan, updating a fitness threshold in each successive iteration, as described above, is equivalent to changing an original clause. An original clause may also be changed in response to a change in constraints resulting from a change in the environment of the problem. The SAT solver attempts to find a new plan by resolving the changed and unchanged original clauses. To this end, the present back-tracking algorithms assume that the root conflict clauses (i.e., the learned clauses that can avoid repeating a conflict) are logical implications of the original clauses of the formula being solved. Therefore, when one or more original clauses are changed, in a subsequent iteration all conflict causes are relearned, requiring significant time. As such, in complex resource assignment and employment problems, existing planning approaches may need to search a large space of several potentially feasible plans. Accordingly, planning at each level of fitness by resolving the modified and unmodified clauses can take a significant time, rendering the back-tracking method impractical or unusable in situations requiring a rapid solution.